Iof proof for Lemma let wf:
1. A : Type
2. B : Type
3. a : A
4. b : A
B
(
x.b(x))(a) 
B
by % (Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 1000:n)) (first_tok :t) inil_term)
bshould have got this, but type inf failed
on untyped lambda... %
Reduce 0
Re1:
Re1:
b(a) B
Re.